Nuprl Lemma : weak-antecedent-function_wf
11,40
postcript
pdf
es
:ES,
P
,
Q
:(E
),
f
:({
e
:E|
P
(
e
)}
E).
Q
==
f
==
P
latex
Definitions
t
T
,
f
(
a
)
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
e
c
e'
,
x
:
A
B
(
x
)
,
,
P
&
Q
,
E
,
{
x
:
A
|
B
(
x
)}
,
b
,
ES
,
Q
==
f
==
P
,
Type
Lemmas
es-E
wf
,
event
system
wf
,
es-causle
wf
origin
es:ES, P, Q:(E
), f:({e:E| P(e)} E). Q 
==f== P 
es:ES, P, Q:(E), f:({e:E| P(e)} E). Q ==f== P TB(x)x:A. B(x)
e'
B(x)
b==f== P